Meeting Pearls 1

home *** CD-ROM | disk | FTP | other *** search

/ Meeting Pearls 1 / Meeting Pearls Vol 1 (1994).iso / installed_progs / text / faqs / meta-lang-faq < prev next >

Wrap

Internet Message Format | 1994-04-22 | 37.0 KB

Subject: Comp.Lang.ML FAQ [Monthly Posting] Newsgroups: comp.lang.ml,comp.answers,news.answers From: jgmorris@cs.cmu.edu (Greg Morrisett) Date: Thu, 21 Apr 1994 14:57:16 GMT Archive-name: meta-lang-faq Last-modified: 1994/03/18 COMP.LANG.ML Frequently Asked Questions and Answers (compiled by Dave Berry and Greg Morrisett) Please send corrections, additions, or comments regarding this list to comp-lang-ml-request@cs.cmu.edu. Changes since last month: ------------------------ <none> Contents: --------- 1. What is ML? 2. Where is ML discussed? a. Comp.Lang.ML b. SML-LIST c. CAML-LIST 3. What implementations of ML are available? a. quick summary (by machine/OS) b. Poly/ML c. Standard ML of New Jersey d. Poplog ML e. ANU ML f. MicroML g. sml2c h. Caml Light i. ML Kit Compiler 4. Unsupported SML/NJ Ports a. MS-DOS/Windows b. Linux c. OS/2 5. Where can I find documentation on ML? a. The Definition b. Textbooks 6. Where can I find ML library code? 7. Theorem Provers and ML 8. Miscellaneous Questions a. How do I write the Y combinator in SML? b. Where can I find an X-windows interface to SML? c. How do I call a C function from SML/NJ? d. How do I fix the emacs mode to work with emacs 19? -------------------------------------------------------------------------- 1. What is ML? ML (which stands for Meta-Language) is a family of advanced programming languages with [usually] functional control structures, strict semantics, a strict polymorphic type system, and parametrized modules. It includes Standard ML, Lazy ML, CAML, CAML Light, and various research languages. Implementations are available on many platforms, including PCs, mainframes, most models of workstation, multi-processors and supercomputers. ML has many thousands of users, is taught at many universities (and is the first programming language taught at some). -------------------------------------------------------------------------- 2. Where is ML discussed? COMP.LANG.ML ------------ comp.lang.ml is a moderated usenet newsgroup. The topics for discussion include but are not limited to: * general ML enquiries or discussion * general interpretation of the definition of Standard ML * applications and use of ML * announcements of general interest (e.g. compiler releases) * discussion of semantics including sematics of extensions based on ML * discussion about library structure and content * tool development * comparison/contrast with other languages * implementation issues, techniques and algorithms including extensions based on ML Requests should be sent to: comp-lang-ml@cs.cmu.edu Administrative mail should be sent to: comp-lang-ml-request@cs.cmu.edu Messages sent to the newsgroup are archived at CMU. The archives can be retrieved by anonymous ftp from internet sites. Messages are archived on a year-to-year basis. Previous years' messages are compressed using the Unix "compress" command. The current year's messages are not compressed. ftp pop.cs.cmu.edu username: anonymous password: <username>@<site> binary cd /usr/jgmorris/sml-archive get sml-archive.<year>.Z quit zcat sml-archive.<year>.Z (Pop's IP address is 128.2.205.205). Individual messages can also be accessed in the directories /usr/jgmorris/mh-sml-archive/<year>-sml. SML-LIST -------- The SML-LIST is a mailing list that exists for people who cannot (or do not want to) read the Usenet COMP.LANG.ML newsgroup. Messages are crossposted from COMP.LANG.ML to the SML-LIST and vice-versa. You should ask to join the SML-LIST _only if_ you cannot (or do not want to) read the Usenet COMP.LANG.ML newsgroup. To send a message to the SML-LIST distribution, address it to: sml-list@cs.cmu.edu (sites not connected to the Internet may need additional routing.) Administrative mail such as requests to add or remove names from the distribution list should be addressed to sml-list-request@cs.cmu.edu CAML-LIST --------- The Caml language, a dialect of ML, is discussed on the Caml mailing list. To send mail to the Caml mailing list, address it to: caml-list@margaux.inria.fr Administrative mail should be addressed to: caml-list-request@margaux.inria.fr ALT.LANG.ML ----------- Another venue for ML-related discussion is the Netnews group alt.lang.ml, though this has seen relatively little traffic. -------------------------------------------------------------------------- 3. What implementations of ML are available and where can I find them? (Note, this information may be out of date.) Quick Summary: System full SML? contact Platforms ------ --------- ------------ ------------------------------ Poly/ML yes ahl@ahl.co.uk SPARC/SUNOS, SPARC/Solaris SML/NJ yes dbm@resarch.att.com Unix/Sparc,Mips,Vax,680x0, ftp research.att.com I386/486,HPPA,RS/6000, MacOS/MacII ftp.rz.uni-karlsruhe.de Linux (including binaries) ftp-os2.nmsu.edu OS/2 (including binearies) PoplogML yes isl@integ.uucp, VMS/Vax, Unix/Vax,Suns,Sparcs, alim@uk.ac.sussex.cogs, Solbourne, Sequent Symmetry, pop@cs.umass.edu HP M680?0, Apollo, AUX/MacII Edinburgh core ftp ftp.dcs.ed.ac.uk 32-bit machines (bytecode) ftp ftp.informatik.uni-muenchen.de PC 80386SX+ ANU ML core mcn@anucsd.anu.edu.au Sun-3, Ultrix/Vax, Pyramid, AUX/MacII MicroML core olof or mahler @cs.umu.se PC 80286+ (bytecode) ftp ftp.cs.umu.se sml2c yes dtarditi@cs.cmu.edu 32-bit Unix machines (C code) ftp dravido.soar.cs.cmu.edu Caml Light coreish caml-light@margaux.inria.fr 32-bit Unix, Mac, PC 8086, ftp ftp.inria.fr PC 80386 (bytecode) Kit yes ftp ftp.diku.dk (Requires another SML compiler ftp ftp.dcs.ed.ac.uk to build binaries) Details: Poly/ML: Poly/ML produces native code for SPARC systems under either SUNOS (4.1) or Solaris (2.3). A PC version is currently under development. Poly/ML uses a persistent store and supports arbitrary precision integer arithmetic. The Motif Edition of Poly/ML comes with a make system, an X11/Xlib interface, and a OSF/Motif interface. Non-standard extensions include concurrent processes and an associated message-passing scheme. Poly/ML is a commercial product from Abstract Hardware Ltd. (ahl@ahl.co.uk). The price of the Motif edition is 1250 pounds for an academic site licence or 3500 pounds per machine for commercial users. Multiple and site licences are available by negotiation. Standard ML of New Jersey: Standard ML of New Jersey was developed jointly at AT&T Bell Laboratories and Princeton University. It is an open system (source code is freely available) implemented in Standard ML. Version 0.93 of SML/NJ generates native code for 68020, SPARC, and MIPS (big and little endian), I386/486, HPPA(HP9000/700), and RS/6000 architectures under various versions of the Unix operating system (SunOS, Ultrix, Mach, Irix, Riscos, HPUX, AIX, AUX, etc.), and on the MacIntosh OS (Mac II, System 7.x, min 12MB ram). Version 0.75 runs on the Vax under Ultrix, BSD, and Mach. SML/NJ comes with a source-level debugger, profiler, gnu emacs interface, ML implementations of LEX, YACC, and Twig, separate compilation facilities, Concurrent ML, the eXene X Window library, and the SML/NJ library. It runs interactively and can produce stand-alone executable applications. Non-standard extensions include typed first-class continuations, Unix signal handling, and higher-order functors. SML/NJ is copyrighted by AT&T but the system, including source code, is freely distributable. It is available by anonymous ftp from research.att.com (192.20.225.2) and princeton.edu (128.112.128.1). Login as "anonymous" with your user name as password. Put ftp in binary mode and copy the (compressed tar) files you need from the directory dist/ml (pub/ml on princeton.edu). You only need the 93.mo.*.tar.Z files for your machine in addition to the 93.src.tar.Z. (You might also want the 93.release-notes.[ps|txt], 93.tools.tar.Z, 93.doc.tar.Z, and smlnj-lib-0.2.tar.Z files.) Alternatively mail dbm@research.att.com. In the UK, SML/NJ is available from the LFCS. There are unsupported ports of SML/NJ to other platforms, including Linux, FreeBSD, OS/2, and Microsoft Windows 3.1. See the "Unsupported SML/NJ Ports" section for details. Poplog ML: Standard ML is supported as part of the Poplog system, which also provides incremental compilers for Pop-11, Common Lisp and Prolog in a common environment with shared data-structures, so that mixed language programming is possible. The integrated editor and HELP mechanism support online teaching aids. Poplog comes with an X Windows interface. Poplog is available for VAX+VMS, VAX+Ultrix, VAX+Bsd 4.2/3, Sun-2,3,4, Sun386i, SPARCstation, Solbourne, Sequent Symmetry (with Dynix), HP M680?0+Unix workstations and Apollo+Unix. Versions for MAC-II with A/UX, DECstation 3100 and MIPS will be available shortly. UK educational users should contact the School of Cognitive and Computing Sciences, University of Sussex (alim@uk.ac.sussex.cogs). People in the USA or Canada should contact Computable Functions Inc. (pop@cs.umass.edu). All others should contact Integral Solutions Ltd. (isl@integ.uucp). UK academic prices start at 600 pounds. Non-UK academic prices start at 1125 pounds. Commercial prices start around 2,000 pounds for an ML-only version or 7,500 pounds for the full Poplog system. Edinburgh ML 4.0: Edinburgh ML 4.0 is an implementation of the core language (without the module system). It uses a bytecode interpreter, which is written in C and runs on any machine with 32 bit words, a continuous address space and a correct C compiler. Ports to various 16 bit machines are underway. The bytecode interpreter can be compiled with switches to avoid the buggy parts of the C compilers that we've used it with (as far as I know none of them worked correctly). Edinburgh ML 4.0 is available from the LFCS. A port to PCs with 386SX processors or better is available by FTP from ftp.informatik.uni-muenchen.de, in the file pub/sml/ibmpc/edml3864.exe. Contact Joern Erbguth (jnerbgut@cip.informatik.uni-erlangen.de) for more information. Some information from Felix von Normann follows: There are other Edinburgh (PC-)ports of ML including an OS/2 2.x, an OS/2 PM and a Dos version. A new version has just been made ready and is available at forwiss.uni-passau.de (132.231.1.10) in pub/ibmpc/os2/lang/sml/sml04.zip. It is about 360K long (short?). All 3 programs have in common (all in one .zip): - true 32 Bit applications - easy to install, easy to use - As far as I know they work stable (except the DOS version working as a Windows window [you can use it with Windows but it crashes on *exit*]) - they don't require expensive hardware (and they don't need a co-processor) To be more specific: OS/2 PM OS/2 DOS OS >= OS/2 2.0+ServPak >= OS/2 2.0 >= DOS 5.0 Edit PM, GUI, Standard command history integrated editor (cut&paste) HW >= 386/33, 8MB >= 386/33 4MB >= 386sx, 2MB lots of MB and fast graphics ad. recommened Help online online (+ML ref. in german) ANU ML ANU ML is descended from Cardelli's ML Pose 3. It implements the core language of the standard and an old version of modules. It incrementally compiles to native code on Sun-3, Vax/Ultrix, Pyramid and MacII/AUX. (It is intended to standardize modules and do the port to Sun-4 in the near future.) ANU ML has a program development system with strong support for debugging (tracing, automatic retesting etc.) and has been extended with a built-in type complex. ANU ML is still considered to be in beta release since exceptions have been standardized quite recently. It is available from Malcolm Newey, CS Dept., Australian National University (mcn@anucsd.anu.edu.au) by arrangement; soon to be available by ftp. MicroML MicroML is an interpreter for a subset of SML that runs on IBM PCs, from the Institute of Information Processing at the University of Umea in Sweden. It implements the core language except for records. A 80286 processor or better is recommended. MicroML is available as an alpha-release by anonymous ftp from ftp.cs.umu.se /pub/umlexe01.uue. There are several known bugs in the current version. For more information contact Olof Johansson (olof@cs.umu.se) or Roger Mahler (mahler@cs.umu.se). sml2c sml2c is a Standard ML to C compiler. It is based on SML/NJ and shares its front-end and most of the runtime system. sml2c is a batch compiler and compiles only module-level declarations. It does not support SML/NJ style debugging and profiling. sml2c is easily portable and has been ported to IBM RT, Decstation 3100, Decstation 5000, Omron Luna 88k, sun-3, sun-4 and a 486-based machine (running Mach). The generated code is highly portable and makes very few assumptions about the target machine or the C compilers available on the target machine. The runtime system, which it shares with the SML/NJ has several machine and operating system dependencies. sml2c has eliminated some of these dependencies by using portable schemes for garbage collection and for freezing and restarting programs. sml2c is available by anonymous ftp from dravido.soar.cs.cmu.edu (128.2.220.26). Log in as anonymous, send username@node as password. The compressed tar file sml2c.tar.Z can be found in /usr/nemo/sml2c. The local ftp software will allow you to change directory only to /usr/nemo/sml2c. The size of the tar file is about 3 Meg. The size of the uncompressed distribution is about 12 Meg. Caml Light Caml Light is a portable, bytecode interpreter for a subset of CAML, a dialect of ML. Some features of Caml Light include separate compilation, streams and stream parsers, ability to link to C code, and tools for building libraries and toplevel systems. The PC versions provide line editing and the 80386 port is VCPI-compliant. The Unix version should work on any modern workstation. We have tested it on Sun 3 and 4, DecStations, HP 9000/700 and 9000/350, IBM RS/6000, SGI Indigo, Sony News, Next cubes, and some more exotic machines. The Macintosh version is now a standalone Macintosh application, and no longer requires the Macintosh Programmer's Workshop. (Well, at least for the toplevel environment; the batch compilers still run under MPW.) The application provides some graphics primitives. The PC version still comes in two flavors, one that run on any PC, but is severely limited by the 640K barrier, and one that run on 80386 or 80486 PC's in 32 bit protected mode to circumvent these limitations. Both versions now provide the same graphics primitives as the Macintosh version. Ports to OS/2 and to the Amiga are in progress. The version 0.6 of the Caml Light system has been released, and is available by anonymous FTP from: host: ftp.inria.fr (192.93.2.54) directory: lang/caml-light Summary of the files: README More detailed summary cl6unix.tar.Z Unix version cl6macbin.sea.hqx Binaries for the Macintosh version cl6macsrc.sea.hqx Source code for the Macintosh version cl6pc386bin.zip Binaries for the 80386 PC version cl6pc386src.zip Source code for the 80386 PC version cl6pc86bin.zip Binaries for the 8086 PC version cl6pc86src.zip Source code for the 8086 PC version cl6refman.* Reference manual, in various formats cl6tutorial.* Tutorial, in various formats This release is mostly a bug-fix release and should be compatible with Caml Light 0.5. The main changes are: * Better handling of type abbreviations. * Debugging mode (option -g to camlc and camllight) to get access to the internals of module implementations. * New library modules: genlex generic lexical analyser set applicative sets over ordered types map applicative maps over ordered types baltree balanced binary trees over ordered types * "compile" command at toplevel (especially useful in the Macintosh version). * New contributed libraries and tools: camlmode Emacs editing mode for Caml Light mletags Indexing of Caml Light source files for use with Emacs "tags" search_isos Search libraries by types (modulo isomorphisms) libgraph X implementation of the portable graphics library libnum Arbitrary-precision arithmetic libstr String operations, regular expressions * The 80386 PC version is now DPMI-compliant, hence it can run under Windows (in text mode inside a DOS windows and with no graphics, though). * More examples, including those from the book "Le langage Caml". General questions and comments of interest to the Caml community should be sent to caml-list@margaux.inria.fr, the Caml mailing list. (see question 3 above for details.) ML Kit Compiler The ML Kit is a straight translation of the Definition of Standard ML into a collection of Standard ML modules. For example, every inference rule in the Definition is translated into a small piece of Standard ML code which implements it. The translation has been done with as little originality as possible - even variable conventions from the Definition are carried straight over to the Kit. If you are primarily interested in executing Standard ML programs efficiently, the ML Kit is not the system for you! (It uses a lot of space and is very slow.) The Kit is intended as a tool box for those people in the programming language community who may want a self-contained parser or type checker for full Standard ML but do not want to understand the clever bits of a high-performance compiler. We have tried to write simple code and module interfaces; we have not paid any attention to efficiency. The documentation is around 100 pages long and is provided with the Kit. It explains how to build, run, read and modify the Kit. It also describes how typing of flexible records and overloading are handled in the Kit. The ML Kit is written by Nick Rothwell, David N. Turner, Mads Tofte and Lars Birkedal at Edinburgh and Copenhagen Universities. The ML Kit is available via anonymous ftp. Here is a sample dialog: ftp ftp.diku.dk ftp ftp.dcs.ed.ac.uk Name: anonymous Name: anonymous Password: <your loginname@host> Password: <your loginname@host> ftp> binary ftp> binary ftp> cd diku/users/birkedal ftp> cd export/ml/mlkit ftp> get README ftp> get README ftp> get COPYING ftp> get COPYING ftp> get src.tar.Z ftp> get src.tar.Z ftp> get doc.tar.Z ftp> get doc.tar.Z ftp> get tools.tar.Z ftp> get tools.tar.Z ftp> get examples.tar.Z ftp> get examples.tar.Z ftp> bye ftp> bye The file README contains installation instructions. Note that no binaries are distributed and that you must build these using either Standard ML of New Jersey, or Poly/ML. -------------------------------------------------------------------------- 6. Unsupported SML/NJ Ports This section describes various ports of SML/NJ (see section 5) that are not directly supported by the NJ folks. MS-DOS/Windows? --------------- (From Dave MacQueen) There is an MS-Windows/MSDOS implementation of Standard ML of New Jersey available by annonymous ftp on research.att.com, directory dist/ml/working/sml-386. This port was done by Yngvi Guttesen at the Danish Technical University in Copenhagen, and it is based on version 0.75 of SML/NJ. The distribution consists of the following four files. -rw-rw-r-- 1 dbm other 417 Feb 16 1993 README -rw-rw-r-- 1 dbm other 51375 Feb 7 1992 doc.tar.Z -rw-rw-r-- 1 dbm other 749105 May 5 1992 mo.386.tar.Z -rw-rw-r-- 1 dbm other 851445 Feb 7 1992 src.tar.Z This Windows port is rather delicate, and when we got it we had a lot of trouble getting it working here at Bell labs. We tried several different machines and finally found one on which it would run (a Gateway 2000 with 16 MB of RAM), though even then it was not very robust or fast. It seemed to be a problem of finding a machine with just the right memory management configuration. I must admit that memory management under Windows is a black art that I am not familiar with, so I have no idea how to characterize the required memory configuration. My conclusion is that the current Windows 3.1/MSDOS environment is so difficult that it would require a major additional investment to have a really useful port. Guttesen did not have a 32 bit C compiler available, so he rewrote the runtime system in assember, which makes it difficult to modify his port. An alternative is to wait for Windows NT (Win32) or OS/2 ports, which may be done in the coming months (a couple of people have independently been working on OS/2 ports recently). Another alternative is to look in directory pub/ml of ftp.dcs.ed.ac.uk, where there are a couple of (partial) implementations of SML that run on PCs. A third alternative is to look into Xavier Leroy's CAML Light. (Details of these are in the comp.lang.ml FAQ message.) However, Guttesen's 386 code generator was used by Mark Leone of CMU as the basis for a port to Unix on Ix86 machines. The current release of SML of New Jersey (0.93) incorporates Intel/Unix support for Mach (used at Carnegie-Mellon University), BSD386 (a product of BSDI?), and 386bsd (a free version of Unix for the PC). There are also versions that run under Linux (available as part of the free Linux distribution) and SVR4, although we have not yet integrated the code supporting Linux and SVR4 into the distributed 0.93 runtime system. Interest has been expressed in a port for SCO Unix, but, as far as we know, no one has done such a port. Very recently Peter Bertelsen of the Technical University of Denmark has done a port to OS2, which is now available on research.att.com, directory dist/ml. Linux? ------ (Thanks to Ralf Reetz, Peter Su, and Mark Leone) Various ftp sites that seem to carry SML/NJ version 0.93 for Linux: ftp.rz.uni-karlsruhe.de:/linux/mirror.tsx/ binaries/usr.bin/njsml.93.bin.z sources/usr.bin/njsml.93.linux.README sources/usr.bin/njsml.93.linux.README.NEW sources/usr.bin/njsml.93.linux.diffs.z sources/usr.bin/njsml.93.src.tar.z ftp@tsx-11.mit.edu:/pub/linux/ sources/usr.bin/njsml.93.src.tar.z ftp.dcs.glasgow.ac.uk? From the README file: Standard ML of New Jersey Version 0.93 for the i386/i486 running Linux, April 23, 1993 __ WHAT SML/NJ is a compiler for the functional programming language Standard ML (SML). It is a fairly complete and robust implementation of ML. __ FILES njsml.93.bin.z - gzip'd binary of njsml (no SourceGroup) njsml-sg.93.bin.z - gzip'd binary of njsml with SourceGroup njsml.93.src.tar.z - minimal sources for NJSML on Linux njsml.93.mo.i386.z - you'll need these also to compile on Linux You can pick up additional tools and goodies from: research.att.com under the "ml" directory. __ HISTORY This is a port of Standard ML of New Jersey (SML/NJ) to Linux. It is based on the work of Mark Leone (mleone@cs.cmu.edu) who did the port for i386/i486 machines. The current binary was compiled using Linux 0.99.7a. Shared lib 4.3.3. This port was done by Sanford Barr (sbarr@cs.sunysb.edu) based on the original port of 0.91 by Hermano Moura (moura@dcs.glasgow.ac.uk) and Andre Santos (andre@dcs.glasgow.ac.uk). __ RECOMMENDED ENV 16M of ram is suggested if you wish to do anything serious with the system. Also, a 386-40 or better would be helpful. __ KNOWN BUGS AND DEFICIENCIES 1 Some minimal precision problems exist when a 387 emulator is used. 2 ML functions System.Directory.listDir and System.Directory.getWD not working at the moment. __ WHERE NJ-SML 0.93 should be available at most major Linux sites. It should also be available in: sbcs.sunysb.edu:/pub/linux by the time you are reading this. OS/2: ----- Standard ML of New Jersey (version 0.93) has been ported to PC's running OS/2. Signal handling is not implemented. This port has been implemented using Mark Leone's code generator for Intel 80386 and the Unix emulator emx, copyright of Eberhard Mattes. SML/NJ is copyright of AT&T Bell Laboratories. There is no warranty of any kind! Requirements: - IBM OS/2 version 2.x - HPFS file system (long file names required) - emx version 0.8g or later - '.mo' files for i386 The port is available for anonymous ftp from research.att.com (in /dist/ml) and, in Europe, from ftp.id.dth.dk (in /pub/bertelsen): 93.os2port.zip Archived with Info-ZIP's Zip utility 93.os2port.tar.Z Archived with GNU's tape archive utility 93.os2port.txt Port announcement & installation guide Please note that the .tar.Z and .zip version of the SML/NJ port are exactly alike and both contain a full source set (but no '.mo' files) for compiling to OS/2 with emx/gcc (not included). The i386 '.mo' archive (93.mo.i386.tar.Z) is available from research.att.com (in /dist/ml) and princeton.edu (in /pub/ml). The emx environment is available from various OS/2 related ftp sites, e.g. ftp-os2.cdrom.com. A binary-only release of this SML/NJ port (no source, interactive system executable only) is also available for anonymous ftp from ftp-os2.cdrom.com. If you have questions concerning this port, please send email to: Peter Bertelsen (c917023@id.dth.dk) Department of Computer Science, Technical University of Denmark FreeBSD: -------- SML/NJ is also available in source and binary format for FreeBSD from freebsd.cdrom.com:/pub/FreeBSD/packages/sml_src.tgz and sml_bin.tgz. The binary package includes EXene and CML as well. -------------------------------------------------------------------------- 5. Where can I find documentation on SML? THE DEFINITION. Robin Milner, Mads Tofte and Robert Harper The Definition of Standard ML MIT, 1990. ISBN: 0-262-63132-6 Robin Milner and Mads Tofte Commentary on Standard ML MIT, 1991 ISBN: 0-262-63137-7 TEXTS. Jeffrey D. Ullman Elements of ML Programming Prentice-Hall, 1993 (Oct. 15) ISBN: 0-13-184854-2 (See Comp.Lang.ML archives, message from Ullman dated 22 Sep 1993 for chapter headings.) Rachel Harrison Abstract Data Types in Standard ML John Wiley & Sons, April 1993 ISBN: 0-471-938440 Ake Wikstrom Functional Programming Using Standard ML Prentice Hall 1987 ISBN: 0-13-331661-0 Chris Reade Elements of Functional Programming Addison-Wesley 1989 ISBN: 0-201-12915-9 Lawrence C Paulson ML for the Working Programmer Cambridge University Press 1991 ISBN: 0-521-39022-2 Stefan Sokolowski Applicative High Order Programming: The Standard ML perspective Chapman & Hall 1991 ISBN: 0-412-39240-2 0-442-30838-8 (USA) Ryan Stansifer ML Primer Prentice Hall, 1992 ISBN 0-13-561721-9 Colin Myers, Chris Clack, and Ellen Poon Programming with Standard ML Prentice Hall, 1993 ISBN 0-13-722075-8 (301pp) The following report is available from the LFCS (Lorraine Edgar, lme@dcs.ed.ac.uk) and costs 5 pounds or 10 US dollars. It covers all of Standard ML. The report is also available via the World Wide Web off of http://www.cs.cmu.edu:8001/afs/cs.cmu.edu/project/fox/mosaic/HomePage.html. Alternatively, the report can be ftp'd from ftp.cs.cmu.edu as the file /afs/cs/project/fox/mosaic/intro-notes.ps. Robert Harper Introduction to Standard ML LFCS Report Series ECS-LFCS-86-14 Laboratory for Foundations of Computer Science Department of Computer Science University of Edinburgh Nov. 1986 (revised Jan. 1989 by Nick Rothwell and Kevin Mitchell) The following report is available from the LFCS (Lorraine Edgar, lme@dcs.ed.ac.uk) and costs 2.50 pounds or 5 US dollars for single copies and 1.50 pounds or 3 dollars when bought in bulk. It includes an introduction to Standard ML and 3 lectures on the modules system. Mads Tofte Four Lectures on Standard ML LFCS Report Series ECS-LFCS-89-73 Laboratory for Foundations of Computer Science Department of Computer Science University of Edinburgh March 1989 The following report is available from the LFCS (Lorraine Edgar, lme@dcs.ed.ac.uk) and is free. It introduces Extended ML, a language for writing (non-executable) specifications of Standard ML programs and for formally developing Standard ML programs from such specifications. Don Sannella Formal program development in Extended ML for the working programmer. LFCS Report Series ECS-LFCS-89-102 Laboratory for Foundations of Computer Science Department of Computer Science University of Edinburgh December 1989 -------------------------------------------------------------------------- 6. Where can I find library code? The Edinburgh SML Library provides a consistent set of functions on the built-in types of the language and on vectors and arrays, and a few extras. It includes a "make" system and a consistent set of parsing and unparsing functions. The library consists of a set of signatures with sample portable implementations, full documentation, and implementations for Poly/ML, Poplog ML and SML/NJ that use some of the non-standard primitives available in those systems. It is distributed with Poly/ML, Poplog ML and Standard ML of New Jersey. It is also available from the LFCS. The library documentation is available as a technical report from the LFCS (Lorraine Edgar, lme@dcs.ed.ac.uk) and costs 5 pounds or 10 US dollars. The LaTeX source of the report is included with the library. Dave Berry The Edinburgh SML Library LFCS Report Series ECS-LFCS-91-148 Laboratory for Foundations of Computer Science Department of Computer Science University of Edinburgh April 1991 The SML/NJ Library is distributed with the SML of New Jersey compiler. It provides a variety of utilities such as 2-dimensional arrays, sorting, sets, dictionaries, hash tables, formatted output, Unix path name manipulation, etc. The library compiles under SML/NJ but should be mostly portable to other implementations. -------------------------------------------------------------------------- 7. Theorem Provers and ML (Collected by Paul Black, pblack@cs.berekeley.edu. Thanks Paul!) - LCF (Edinburgh LCF and Cambridge LCF) * written in the original Edinburgh dialect of ML from which SML developed. "Logic and Computation: Interactive Proof with Cambridge LCF" also by Lawrence C. Paulson. - Lego (LFCS, Edinburgh Univ., SML) * originally developed in CAML * latest version (5) now runs under SML/NJ * only higher-order resolution * available via anon. ftp from ftp.dcs.ed.ac.uk:/pub/lego - HOL90 Authors = Konrad Slind, Elsa Gunter elsa@research.att.com, slind@informatik.tu-muenchen.de http://lal.cs.byu.edu/lal/hol-documentation.html hol90 is a free implementation in SML/NJ of Mike Gordon's HOL logic (a polymorphic version of Church's Simple Type Theory). The system provides a lot of automated support including: - a powerful rewriting package; - pre-installed theories for booleans, products, sums, natural numbers, lists, and trees; - definition facilities for recursive types and recursive functions over those types (mutual recursion is also handled); - extensive libraries for strings, sets, group theory, integers, the real numbers, wellordered sets, automatic solution of goals involving linear arithmetic, tautology checking, inductively defined predicates, Hoare logic, Chandy and Misra's UNITY theory, infinite state automata, and many others. The HOL community has a lively mailing list accessible at info-hol-request@leopard.cs.byu.edu and a yearly user's meeting that alternates between Europe and North America. hol90 is available by anonymous ftp from machine = ftp.informatik.tu-muenchen.de directory = local/lehrstuhl/nipkow/hol90/hol90.6.tar.Z or machine = research.att.com directory = dist/ml/hol90/hol90.6.tar.Z - NuPrl (from Bob Constable`s group at Cornell) - Isabelle (Lawrence C. Paulson, Cambridge Univ. ) * has rewriting, but not many decision procedures. It does has things like model elimination-based decision procedures. * a generic automatic theorem prover i.e. you can program it to the logic system/proof system you want. Already has the following subsystems already implemented: i) FOL - first order logic ii) HOL - higher order logic iii) LCF - Logic of computable functions iv) LK - Gentzen system LK v) Modal - Modal logic systems T, S4, S43 vi) ZF - Zermelo-Fraenkel set theory * ftp from <gannet.cl.cam.ac.uk> - MERILL (Brian Matthews, U. of Glasgow & Rutherford Appleton Laboratory) * written in standard ML * a general purpose order-sorted equational reasoning system * Allows the user to declare their own object language, allows AC-rewriting and AC-unification of terms and equations, has several completion algorithms, is built on a hierarchy of types known as Order-Sorting, and allows the user to try different termination methods. * available via anonymous ftp from the University of Glasgow, ftp address: ftp.dcs.glasgow.ac.uk (130.209.240.50) * Brian Matthews, brian@dcs.glasgow.ac.uk or bmm@inf.rl.ac.uk - FAUST (Karlsruhe) * a HOL add-on written in ML. * ftp from goethe.ira.uka.de (129.13.18.22) - Alf * written in SML * An implementation of Martin-Lofs type theory with dependent types * Proof editor * available by anonymous ftp from cs.chalmers.se * only higher-order resolution - Coq * written in Caml-Light (but Caml-Light and SML are VERY similar) * no serious automated reasoning subsystems (other than higher-order resolution), but has a VERY nice package for program verification. * available via anon. ftp from ftp.inria.fr:/INRIA/coq/V5.8 * possible contact: Chet Murthy <murthy@cs.cornell.edu> - ICLHOL/ProofPower (ICL Secure Systems) * a commercial system using a reimplementation of HOL in SML * contact ProofPower-server@win.icl.co.uk - Lamdba/DIALOG (Abstract Hardware Ltd) * a commercial tool written in Poly/ML, neither of which is free. - Elf (Frank Pfenning, Carnegie Mellon Univ.) * Elf is a higher-order logic programming language based on the LF Logical Framework. * Elf is not a theorem prover per-se, but is useful for specifying and proving properties of programming languages, logics, and their implementations. A number of examples are provided with the distribution. * The Elf implementation is written in SML/NJ and should be easily portable to other SML implementations. * Elf can be ftp'd from alonzo.tip.cs.cmu.edu (128.2.209.194) in the directory /afs/cs/user/fp/public. * A bibliography and a collection of papers regarding LF and Elf can be found in the directory /afs/cs/user/fp/public/elf-papers. * There is an Elf mailing list. Contact elf-request@cs.cmu.edu to join. * For further information, contact Frank Pfenning (fp@cs.cmu.edu). References "ML for the Working Programmer" by Lawrence C. Paulson contains a small first-order theorem prover. Paulson also has a good chapter on writing theorem provers in ML in "Handbook of logic in computer science", Edited by: S. Abramsky, Dov M. Gabbay, and T.S.E. Maibaum. Oxford : Clarendon Press, 1992-. CALL#: QA76 .H2785 1992 Others We have an automated theorm proving system here at the University of Tasmania, but it is still under development, currently riddled with bugs and has an obscure "input language"; aside from those minor problems, it'd be perfect... La Monte H. Yarroll <piggy@hilbert.maths.utas.edu.au> Edinburgh's Concurrency Workbench and Sussex's Process Algebra Mauipulator are also ML systems of note, though neither are interactive theorem provers. -------------------------------------------------------------------------- 8. Miscellaneous How do I write the Y combinator in SML without using a recursive definition (i.e. "fun" or "let rec")? datatype 'a t = T of 'a t -> 'a val y = fn f => (fn (T x) => (f (fn a => x (T x) a))) (T (fn (T x) => (f (fn a => x (T x) a)))) Where can I find an X-Windows interface to SML? Poly/ML, Poplog/ML, and SML/NJ all come with X-Windows interfaces. See the appropriate entries under section 3. In addition, Poly/ML interfaces to the industry standard OSF/Motif toolkit. How do I call a C function from SML/NJ? See the file runtime/cfuns.c for example C functions that are in the runtime and callable from ML. You have to enter the function into a table at the end of the file along with a string. You use the function System.Unsafe.CInterace to look up the function, using the string as the key. Note that you'll need to convert ML values to C representations and back. You'll have to rebuild the compiler using makeml. How do I get the emacs mode to work with Emacs version 19? Add these three lines at the top of your `sml-init.el' file: - ----- BEGIN addition ; emacs 19 doesn't have `make-shell', which sml-shell needs, so get it ; when necessary. 12 Oct 1993 M-J. Dominus (mjd@saul.cis.upenn.edu) (autoload 'make-shell "make-shell" "Make and initialize shell buffer for SML." nil) - ----- END addition They tell emacs to load the file `make-shell.el' when it needs to use the `make-shell' function. Then install this file as `make-shell.el' somewhere on your load path, probably in your emacs `site-lisp' directory: